//==============================================================================
//	
//	Copyright (c) 2002-
//	Authors:
//	* Vincent Nimal <vincent.nimal@comlab.ox.ac.uk> (University of Oxford)
//	* Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford)
//	
//------------------------------------------------------------------------------
//	
//	This file is part of PRISM.
//	
//	PRISM is free software; you can redistribute it and/or modify
//	it under the terms of the GNU General Public License as published by
//	the Free Software Foundation; either version 2 of the License, or
//	(at your option) any later version.
//	
//	PRISM is distributed in the hope that it will be useful,
//	but WITHOUT ANY WARRANTY; without even the implied warranty of
//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
//	GNU General Public License for more details.
//	
//	You should have received a copy of the GNU General Public License
//	along with PRISM; if not, write to the Free Software Foundation,
//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
//	
//==============================================================================

package com.prism.e4.rcp.simulator.method;

import com.prism.e4.rcp.parser.ast.Expression;
import com.prism.e4.rcp.prism.PrismException;
import com.prism.e4.rcp.simulator.sampler.Sampler;

/**
 * Classes to control simulation-based (approximate/statistical) model checking.
 */
public abstract class SimulationMethod implements Cloneable {
	/**
	 * Get the (short) name of this method.
	 */
	public abstract String getName();

	/**
	 * Get the (full) name of this method.
	 */
	public abstract String getFullName();

	/**
	 * Reset the status of this method (but not values of any parameters that
	 * have been set). Typically called if this instance is going to be re-used
	 * for another run of approximate verification.
	 */
	public abstract void reset();

	/**
	 * Compute the missing parameter (typically there are multiple parameters,
	 * one of which can be left free) *before* simulation. This is not always
	 * possible - sometimes the parameter cannot be determined until afterwards.
	 * This method may get called multiple times.
	 * 
	 * @throws PrismException
	 *             if the parameters set so far are invalid.
	 */
	public abstract void computeMissingParameterBeforeSim()
			throws PrismException;

	/**
	 * Set the Expression (property) that simulation is going to be used to
	 * approximate. It will be either an ExpressionProb or ExpressionReward
	 * object. All constants should have already been defined and replaced.
	 * 
	 * @throws PrismException
	 *             if property is inappropriate somehow for this method.
	 */
	public abstract void setExpression(Expression expr) throws PrismException;

	/**
	 * Compute the missing parameter (typically there are multiple parameters,
	 * one of which can be left free) *after* simulation. (Sometimes the
	 * parameter cannot be determined before simulation.) This method may get
	 * called multiple times.
	 */
	public abstract void computeMissingParameterAfterSim();

	/**
	 * Get the missing (computed) parameter. If it has not already been computed
	 * and this can be done *before* simulation, calling this method will
	 * trigger its computation. If it can only be done *after*, an exception is
	 * thrown.
	 * 
	 * @return the computed missing parameter (as an Integer or Double object)
	 * @throws PrismException
	 *             if missing parameter is not and cannot be computed yet or if
	 *             the parameters set so far are invalid.
	 */
	public abstract Object getMissingParameter() throws PrismException;

	/**
	 * Get the parameters of the simulation (including the computed one) as a
	 * string.
	 */
	public abstract String getParametersString();

	/**
	 * Determine whether or not simulation should stop now, based on the
	 * stopping criteria of this method, and the current state of simulation
	 * (the number of iterations so far and the corresponding Sampler object).
	 * Note: This method may continue being called after 'true' is returned,
	 * e.g. if multiple properties are being simulated simultaneously.
	 * 
	 * @param iters
	 *            The number of iterations (samples) done so far
	 * @param sampler
	 *            The Sampler object for this simulation
	 * @return true if the simulation should stop, false otherwise
	 */
	public abstract boolean shouldStopNow(int iters, Sampler sampler);

	/**
	 * Get an indication of progress so far for simulation, i.e. an approximate
	 * value for the percentage of work (samples) done. The value is a multiple
	 * of 10 in the range [0,100]. This estimate may not be linear (e.g. for
	 * CI/ACI where 'iterations' is computed). It is assumed that this method is
	 * called *after* the call to shouldStopNow(...). Note: The iteration count
	 * may exceed that dictated by this method, e.g. if multiple properties are
	 * being simulated simultaneously. TODO: check methods for this
	 * 
	 * @param iters
	 *            The number of iterations (samples) done so far
	 * @param sampler
	 *            The Sampler object for this simulation
	 */
	public abstract int getProgress(int iters, Sampler sampler);

	/**
	 * Get the (approximate) result for the property that simulation is being
	 * used to approximate. This should be a Boolean/Double for
	 * bounded/quantitative properties, respectively.
	 * 
	 * @param sampler
	 *            The Sampler object for this simulation
	 * @throws PrismException
	 *             if we can't get a result for some reason.
	 */
	public abstract Object getResult(Sampler sampler) throws PrismException;

	/**
	 * Get an explanation for the result of the simulation as a string.
	 * 
	 * @param sampler
	 *            The Sampler object for this simulation (e.g. to get mean)
	 * @throws PrismException
	 *             if we can't get a result for some reason.
	 */
	public abstract String getResultExplanation(Sampler sampler)
			throws PrismException;

	@Override
	public abstract SimulationMethod clone();

}

// ------------------------------------------------------------------------------